When designing correct-by-construction controllers for autonomous collectives, three key challenges are the task specification, the modelling, and its use at practical scale. In this paper, we focus on a simple yet useful abstraction for high-level controller synthesis for robot collectives with optimisation goals (e.g., maximum cleanliness, minimum energy consumption) and recurrence (e.g., re-establish contamination and charge thresholds) and safety (e.g., avoid full discharge, mutually exclusive room occupation) constraints. Due to technical limitations (related to scalability and using constraints in the synthesis), we simplify our graph-based setting from a stochastic two-player game into a single-player game on a partially observable Markov decision process (POMDP). Robustness against environmental uncertainty is encoded via partial observability. Linear-time correctness properties are verified separately after synthesising the POMDP strategy. We contribute at-scale guidance on POMDP modelling and controller synthesis for tasked robot collectives exemplified by the scenario of battery-driven robots responsible for cleaning public buildings with utilisation constraints.

Attending ICRA is a great opportunity to see many state-of-the-art (and famous?) robots in a single venue. Indeed, a quick trip to the exhibitors' booths is enough to get introduced to the large and diverse group of commercial robots we have today. Yet, one can easily notice that these amazing state-of-the-art robots do not interact with each other. At least they do not do it without human mediation. Although in the exhibitions one can find two or three robots that appear to be joyfully playing together, the reality is that their operators are creating these inter-robot interactions.

"Reweighting rewards in embodied evolution to achieve a balanced distribution of labour," in Proceedings of the 14th European Conference on Artificial Life ECAL 2017 (Cambridge, MA: MIT Press), 44–51.